Nuprl Lemma : sys-antecedent-retraction
13,45
postcript
pdf
es
:ES,
Sys
:AbsInterface(Top),
f
:sys-antecedent(
es
;
Sys
). retraction(E(
Sys
);
f
)
latex
Up
abstract chain replication
Definitions
x
:
A
.
B
(
x
)
,
AbsInterface(
A
)
,
sys-antecedent(
es
;
Sys
)
,
E(
X
)
,
t
T
,
,
T
,
True
,
P
Q
,
SqStable(
P
)
Lemmas
es-causle-interface-retraction
,
es-E
wf
,
assert
wf
,
es-is-interface
wf
,
top
wf
,
es-causle
wf
,
es-E-interface-subtype
rel
,
event
system
wf
,
sq
stable
from
decidable
,
decidable
es-causle
origin
es:ES, Sys:AbsInterface(Top), f:sys-antecedent(es;Sys). retraction(E(Sys);f) es:ES, Sys:AbsInterface(Top), f:sys-antecedent(es;Sys). retraction(E(Sys);f) 
T
T
Q